$\forall$$M$:MsgA, $l$:IdLnk, ${\it tg}$:Id. $\neg$rcv($l$,${\it tg}$) declared in $M$ $\Rightarrow$ ($M$.din($l$,${\it tg}$) $\sim$ Top)